FDL - Nuprl Definition : es-dds

Nuprl Definition : es-dds

11,40

@i discrete ds == fpf-all(Id; id-deq; ds; x,T.es-dtype(es; i; x; T))

clarification:

es-dds(es;i;ds) == fpf-all(Id; id-deq; ds; x,T.es-dtype(es; i; x; T))

Definitions fpf-all(A; eq; f; x,v.P(x;v)), Id, id-deq, es-dtype(es; i; x; T)

FDL editor aliases es-dds

Definitions	fpf-all(A; eq; f; x,v.P(x;v)), Id, id-deq, es-dtype(es; i; x; T)
FDL editor aliases	es-dds